home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / try_2.06.2 < prev    next >
Text File  |  1992-04-03  |  20KB  |  760 lines
  1. %%% TRY
  2. %%% version 2.00.1 (based on try_19.1)
  3. %%%   added equality rewriting
  4. %%% version 2.01.0
  5. %%%   rewrote clauses in all round 0s instead of just session 1 round 0
  6. %%% version 2.01.5
  7. %%%   added code to rewrite asserted clauses
  8. %%% version 2.01.8
  9. %%%   added transformed form of all non-input equations before hyper-linking
  10. %%% version 2.02.2
  11. %%%   asserted pulled out equations at beginning of session
  12. %%% version 2.02.5
  13. %%%   asserted pulled out forms of equations at the beginning of each round
  14. %%% version 2.03.0
  15. %%%   asserted equations for rewrite rules during round 0 (except for session
  16. %%%     1 round 0) in addtion to other rounds
  17. %%% version 2.03.4
  18. %%%   incorporated changes made to clin V1 between 7/31/90 and 10/18/90 which
  19. %%%     are visible externally -- changes to comments, predicate names, and
  20. %%%     variable names are not incorporated
  21. %%% version 2.03.5
  22. %%%   assert equations for rewrite rules only if there are rewrite rules
  23. %%% version 2.03.8
  24. %%%   don't rewrite clauses if proof found durin  hyper-linking
  25. %%%   rewrite clauses in round 0 when necessary
  26. %%% version 2.04.0
  27. %%%   saved input clauses between sessions same as clin 1
  28. %%% version 2.04.1
  29. %%%   determined maximum number of non-ground literals in a clause each round
  30. %%%     (required for equality transform)
  31. %%% version 2.04.3
  32. %%%   rewrote clauses after replacement (as well as before)
  33. %%% version 2.04.4
  34. %%%   no longer pull out equations at the beginning of rounds
  35. %%%   when replacing and rewriting, perform replacement/rewrite repeatedly
  36. %%%     until no change
  37. %%% version 2.04.5
  38. %%%   added equality_transform_by_round flag
  39. %%% version 2.04.6
  40. %%%   added fixed_priority
  41. %%%   fixed bug in code which determines if another round of hyper-linking is
  42. %%%     required
  43. %%% version 2.04.7
  44. %%%   rewrote asserted clauses after unit simplification
  45. %%% version 2.04.8
  46. %%%   added group_detection
  47. %%% version 2.05.0
  48. %%%   don't select a support strategy unless there is a new clause or an
  49. %%%     existing clause has modified the appropriate support
  50. %%% version 2.05.2
  51. %%%   modified the top level structure of clin
  52. %%% version 2.05.3
  53. %%%   added support for Quintus Prolog
  54. %%%   fixed bug which caused loop when proof found in simplification
  55. %%%   modified clin structure so that clause rewriting done before main
  56. %%%     repeat loop and after simplification
  57. %%% version 2.05.5
  58. %%%   modified clin structure so generation of equations from rewrite rules
  59. %%%     done before main repeat loop after clause rewriting
  60. %%%   fixed bug which prevented "satisfiable" result
  61. %%% version 2.05.6
  62. %%%   modified round 0 action
  63. %%%   don't repeat clause generation unless more than 1 clause generation
  64. %%%     modules requested
  65. %%%   moved instance deletion into clause generation loop
  66. %%%   added print after clause generation
  67. %%% version 2.05.7
  68. %%%   terminated clause generation loop if proof found in replacemet
  69. %%% version 2.05.8
  70. %%%   added priority_bound_increment
  71. %%% version 2.06.0
  72. %%%   apply once_replace_rules only once per round
  73. %%%   added clause_generation_loop flag
  74. %%%   added early check for unit conflict
  75. %%%   modified session 1 round 0 processing
  76. %%%   added save_rewrite_rules
  77. %%% version 2.06.1
  78. %%%   added early unit conflict check to rewrite_rewrite_rules
  79. %%% version 2.06.2
  80. %%%   run clause generation loop in session 1 round 0
  81. %%%   added additional time overflow tests
  82. %%%
  83. %%% A round consists of the follow:
  84. %%%
  85. %%%   if round 0, not session 1, no rewrite rules, not group_dectection, and
  86. %%%     not equality_transform_by_round, do nothing
  87. %%%   else
  88. %%%     if not round 0, then 
  89. %%%       hyper-link
  90. %%%       rewrite clauses
  91. %%%     endif
  92. %%%     generate equations from rewrite rules
  93. %%%     repeat
  94. %%%       run group detection
  95. %%%      pullout equations
  96. %%%       do replacements
  97. %%%       run simplification
  98. %%%       rewrite clauses
  99. %%%       generate equations from rewrite rules
  100. %%%       do instance deletion
  101. %%%     until no new clauses generated
  102. %%%    run PC prover
  103. %%%    run small proof checker
  104. %%%   endif
  105. %%%
  106. %%% Note that some of the above steps are controlled via user-specified flags;
  107. %%% not all of the steps may be performed.
  108. %%%
  109. %%% If sliding priority is not specified, hyper-matches are generated
  110. %%%    until done.
  111. %%% If sliding priority is specified, we divide the running into sessions.
  112. %%%    Each session starts with a work unit bound and infinite priority
  113. %%%    bound. If a session fails to find the proof, double the work unit
  114. %%%    bound, and start a new session.
  115. %%%
  116. %%% If do_replacement_once is asserted, then we do top level replacements
  117. %%%    only at round 0.
  118. %%%
  119. %%% If the problem is tried more than once with same time limit, but
  120. %%%     only with different strategies, then we skip round 0.
  121. %%%    However, we have to do replacements before call round 1 if
  122. %%%    do_replacement_once is asserted.
  123. %%%
  124.  
  125. %%% clause_largest_length is very important, we use it in small proof 
  126. %%%     checking and hyper-matching.
  127. %%% If tried_round is 1, this means we are using top level supervisor,
  128. %%%    and the problem we are trying has been tried before with 
  129. %%%    different strategies in same time limit. Since all the calls
  130. %%%    in round 0 have been executed before, we don't execute them again.
  131. %%%     However, we should run top_level_replace if it is specified.
  132. %%%
  133. %%% The replacement, if set, will be executed at round 0 of each session.
  134. %%%
  135.      try :-  not(not(try_fail)).
  136.  
  137.      try_fail :- 
  138.     priority_option,
  139.          assert(round_no(-1)),        % initial value for round number.
  140.          assert(session_no(1)),        % initial value for round number.
  141.     cputime(Time),
  142.     assert(start_time(Time)),
  143.     assert(round_time(Time,-1)),
  144.     assert(pc_time(0)),        % initialize PC time.
  145.     nl,
  146.     write_line(5,'TRY BEGINS:'),
  147.     try_1,
  148.     !.
  149.  
  150. %%% Interative exexution of rounds.
  151.      try_1 :-
  152.     precheck,
  153.     !.
  154.      try_1 :-
  155.        repeated_clause_generation_needed,
  156.        fail.
  157.      try_1 :-
  158.     repeat,
  159.         print_roundheader,
  160.         assert_new_support,
  161.         round_process,
  162.         round_spent_time.
  163.  
  164. %%% Check to see if repeated clause generation is required.
  165.      repeated_clause_generation_needed :-
  166.     not(clause_generation_loop),
  167.         !,
  168.     assert(no_repeated_clause_generation).
  169.      repeated_clause_generation_needed :-
  170.     repeated_clause_generation_needed_1(0,N1),
  171.     repeated_clause_generation_needed_2(N1,N2),
  172.     repeated_clause_generation_needed_3(N2,N3),
  173.     repeated_clause_generation_needed_4(N3,N4),
  174.     repeated_clause_generation_needed_5(N4,N5),
  175.     repeated_clause_generation_needed_6(N5,N6),
  176.     N6 < 2,
  177.     !,
  178.     assert(no_repeated_clause_generation),
  179.     !.
  180.      repeated_clause_generation_needed :-
  181.     abolish(no_repeated_clause_generation,0),
  182.     !.
  183.      repeated_clause_generation_needed_1(N1,N2) :-
  184.     group_detection,
  185.     !,
  186.     N2 is N1 + 1.
  187.      repeated_clause_generation_needed_1(N,N).
  188.      repeated_clause_generation_needed_2(N1,N2) :-
  189.     replacement,
  190.     !,
  191.     N2 is N1 + 1.
  192.      repeated_clause_generation_needed_2(N,N).
  193.      repeated_clause_generation_needed_3(N1,N2) :-
  194.     equality_transformation_by_round,
  195.     !,
  196.     N2 is N1 + 1.
  197.      repeated_clause_generation_needed_3(N,N).
  198.      repeated_clause_generation_needed_4(N1,N2) :-
  199.     unit_resolution,
  200.     !,
  201.     N2 is N1 + 1.
  202.      repeated_clause_generation_needed_4(N,N).
  203.      repeated_clause_generation_needed_5(N1,N2) :-
  204.     auto_orient,
  205.     !,
  206.     N2 is N1 + 1.
  207.      repeated_clause_generation_needed_5(N,N).
  208.      repeated_clause_generation_needed_6(N1,N2) :-
  209.     rwr(_,_,_,_),
  210.     !,
  211.     N2 is N1 + 1.
  212.      repeated_clause_generation_needed_6(N,N).
  213.  
  214. %%% Executing one round.
  215.      round_process :-
  216.     round_no(0),
  217.         not(session_no(1)),
  218.     not(rwr(_,_,_,_)),
  219.     not(group_dection),
  220.     not(equality_transform_by_round),
  221.     round_spent_time,
  222.     !,
  223.     fail.
  224.      round_process :-
  225.     round_no(0),
  226.     !,
  227.     round_process_1.
  228.      round_process :-
  229.     check_hm_round,
  230.     not(prove_result(_)),
  231.         not(time_overflow),
  232.     clause_rewriting,
  233.     not(prove_result(_)),
  234.         not(time_overflow),
  235.     !,
  236.     round_process_1.
  237.      round_process.
  238.      round_process_1 :-
  239.     clause_generation,
  240.     print_after_clause_generation,
  241.     round_process_2.
  242.      round_process_2 :-
  243.     prove_result(_),
  244.     !.
  245.      round_process_2 :-
  246.     time_overflow,
  247.     !.
  248.      round_process_2 :-
  249.     pc_spc,
  250.     !.
  251.      round_process_2 :-
  252.     time_overflow,
  253.     !.
  254.      round_process_2 :-
  255.     not(get_new_supp(_,_)),
  256.     hl_complete.
  257.      round_process_2 :-
  258.     round_spent_time,
  259.     !,
  260.     fail.
  261.     
  262. %%% Generate clauses after hyper-linking.
  263.      clause_generation :-
  264.     rewrite_rule_equations,
  265.     abolish(no_replace_once,0),
  266.     repeat,
  267.         update_oldsentC1,
  268.         run_group_detection,
  269.         clause_generation_1,
  270.         !.
  271.      clause_generation_1 :-
  272.     prove_result(_),
  273.     !.
  274.      clause_generation_1 :-
  275.     time_overflow,
  276.     !.
  277.      clause_generation_1 :-
  278.     transform_equations_round,
  279.     top_level_replace,
  280.     assert_once(no_replace_once),
  281.     run_simplify,
  282.     !.
  283.      clause_generation_1 :-
  284.     time_overflow,
  285.     !.
  286.      clause_generation_1 :-
  287.     clause_rewriting,
  288.     (prove_result(_);time_overflow),
  289.     !.
  290.      clause_generation_1 :-
  291.     rewrite_rule_equations,
  292.     not(inst_del),
  293.     print_after_instdel,
  294.         repeat_clause_generation,
  295.     !.
  296.  
  297. % Fail if we need to repeat clause generation.
  298.      repeat_clause_generation :-
  299.     no_repeated_clause_generation,
  300.     !.
  301.      repeat_clause_generation :-
  302.     not(diff_sentC1),
  303.     !.
  304.  
  305.      run_simplify :-
  306.     prove_result('unsatisfiable'), !.
  307.      run_simplify :-
  308.     simplify,            % if an EC derived.
  309.     assert_tryresult('unsatisfiable'),
  310.     assert_prooftype('US').
  311.  
  312.      run_pcprover :-
  313.     compute_fms(FMS),        % compute fully matched set.
  314.     print_fms(FMS), !,
  315.     pcprove(FMS),
  316.     assert_tryresult('unsatisfiable'),
  317.     assert_prooftype('PC').
  318.  
  319.      run_spc :-
  320.     spc,   
  321.     assert_tryresult('unsatisfiable'),
  322.     assert_prooftype('SP').
  323.  
  324. %%% If the input set has neither positive nor negative clauses,
  325. %%%    and no replacements are specified, then it is satisfiable.
  326.      precheck :-
  327.     check_emptyclause,
  328.     assert_tryresult('unsatisfiable'),
  329.     assert_prooftype('PR'), !.
  330.      precheck :-
  331.     check_emptyset,
  332.     assert_tryresult('satisfiable'), !.
  333.      precheck :-
  334.     \+ replacement,
  335.     \+ have_pn_clauses,
  336.     write_line(5,'No positive or negative clauses !!'),
  337.     assert_tryresult('satisfiable'), !.
  338.  
  339. %%% hm_round can be turned off.
  340.      check_hm_round :-
  341.     do_hyper_linking,
  342.     update_oldsentC,
  343.     hm_round,
  344.     abolish(saved_supp,2),    
  345.     print_ahm, !.
  346.      check_hm_round :- !.
  347.  
  348. %%% Check to see if hyper-linking is done.
  349.      hl_complete :-
  350.     decidably_satisfiable.
  351.      hl_complete :-
  352.     more_session.
  353.  
  354.      pc_spc :-
  355.     check_run_pc.
  356.      pc_spc :-
  357.     run_spc.
  358.     
  359. %%% If UR round, no PC prover.
  360.      check_run_pc :-
  361.     current_support(sup(_,_,_,1)),
  362.     !,
  363.     fail.
  364.      check_run_pc :-
  365.     run_pcprover.
  366.  
  367. %%% If the set is empty.
  368.      check_emptyset :-
  369.     \+ sent_C(_), !.
  370.           
  371. %%% If there is an empty clause.
  372.      check_emptyclause :-
  373.     sent_C(cl(_,_,by([],_,_,_,_),_,_,_,_,_,_)), !.
  374.  
  375. %%% If having positive and negative clauses.
  376.      have_pn_clauses :-
  377.     have_p_clauses, !,
  378.     have_n_clauses.
  379.  
  380. %%% If having positive clauses.
  381.      have_p_clauses :-
  382.     sent_C(cl(_,_,by(Cn1,_,_,_,_),_,_,_,_,_,_)),
  383.     posclause(Cn1).
  384.  
  385. %%% If having negative clauses.
  386.      have_n_clauses :-
  387.     sent_C(cl(_,_,by(Cn1,_,_,_,_),_,_,_,_,_,_)),
  388.     negclause(Cn1).
  389.  
  390.      assert_prooftype(Message) :-
  391.     assert(proof_type(Message)).
  392.  
  393.      assert_tryresult(Result) :-
  394.     assert(prove_result(Result)).
  395.  
  396. %%% Information for fixed and sliding priority.
  397.      priority_option :-
  398.     fixed_priority,
  399.     compute_start_priority_bound(P),
  400.     assert(priority_bound(P)),
  401.     !.
  402.      priority_option :-
  403.     slidepriority,
  404.     compute_start_wu(WU),
  405.     assert(priority_bound(WU)), 
  406.     assert(wu_bound(WU)), 
  407.     assert(total_numhm(0)),
  408.     assert(total_wu(0)), !.
  409.      priority_option.
  410.  
  411. %%% compute the start priority bound.
  412. %%% set by user -- fail.
  413. %%% not set by user -- return maximum priority of input clauses.
  414.     compute_start_priority_bound(P) :-
  415.     start_priority_bound(P).
  416.     compute_start_priority_bound(P) :-
  417.     bagof1(D9e,{D1,D2,D3,D4,D5,D6,D7,D8,D9a,D9b,D9c,D9d}^
  418.         sent_C(cl(D1,D2,D3,D4,D5,D6,D7,D8,pr(D9a,D9b,D9c,D9d,D9e))),
  419.         Ps),
  420.     max_list(Ps,P).
  421.  
  422.      simplify :-
  423.     print_busentC,
  424.     fol_simplify,
  425.     print_ausentC, !.
  426.      simplify :-
  427.     print_ausentC,
  428.     !,
  429.     fail.
  430.  
  431. %%% Obtain the largest number of non-ground literals of clauses.
  432.      clause_largest_length(N) :-
  433.     bagof(NL,{X1,X3,X4,X5,X6,X7,X8,X9}^
  434.         sent_C(cl(X1,NL,X3,X4,X5,X6,X7,X8,X9)),NLs),
  435.     max_list(NLs,N),
  436.     !.
  437.      clause_largest_length(0).
  438.  
  439. %%% Print out header information for a round.
  440.      print_roundheader :-
  441.     session_no(Y),
  442.     inc_roundno(X),            % increment round no.
  443.     nl, tab(15), write('SESSION '), write(Y), 
  444.     tab(10), write('ROUND '), write(X), nl,
  445.     write_line(5,'#######################################################'),
  446.     file_name(File),
  447.     write_line(19,'File Name = ',File),
  448.     relevance_bound(RelBound),
  449.     write_line(17,'Relevance Bound = ',RelBound),
  450.     print_priority_figures, !.
  451.  
  452. %%% Increment round number and assert it.
  453.      inc_roundno(Y) :-
  454.     retract(round_no(X)), Y is X + 1,
  455.     assert(round_no(Y)), !.
  456.  
  457. %%% Print out information if sliding priority is used.
  458.      print_priority_figures :-
  459.     fixed_priority,
  460.     priority_bound(PrioBound),
  461.     write_line(17,'Priority Bound = ',PrioBound), !.
  462.      print_priority_figures :-
  463.     slidepriority,
  464.      wu_bound(WUBound),
  465.     write_line(20,'WU Bound = ',WUBound),
  466.     priority_bound(PrioBound),
  467.     write_line(17,'Priority Bound = ',PrioBound), !.
  468.      print_priority_figures.
  469.  
  470. %%% Print out how much time spent in the past round.
  471.      round_spent_time :-
  472.     round_no(X), Y is X - 1,
  473.     cputime(Time),
  474.     retract(round_time(LT,Y)),
  475.     Used_Time is Time - LT,
  476.     write_line(5,'Time elapsed in this level(s): ',Used_Time),
  477.     assert(round_time(Time,X)), !.
  478.  
  479. %%% We can detect if a problem is really satisfiable.
  480.      decidably_satisfiable :-
  481.     \+ over_priohm, !,
  482.     \+ over_relevance, !,
  483.     \+ over_litbound, !,
  484.     \+ over_numvars,
  485.     assert_tryresult('satisfiable').
  486.  
  487. %%% Determine is time has overflowed.
  488.      time_overflow :-
  489.     is_time_overflow,
  490.     assert_tryresult('time_overflow').
  491.  
  492.      is_time_overflow :-
  493.     start_time(Start_Time),
  494.     real_time_limit(Max_Time),
  495.     cputime(Current_Time),
  496.     Used_Time is Current_Time - Start_Time,
  497.     !,
  498.     Used_Time > Max_Time. 
  499.  
  500. %%% Check if a new session is needed.
  501.      more_session :-
  502.     not(fixed_priority),
  503.     not(slidepriority),
  504.     !,
  505.     assert_tryresult('misc_overflow').
  506.      more_session :-
  507.     check_stopsession.
  508.  
  509. %%% If there are some hyper-matches deleted due to priority overflow,
  510. %%%    do check_maxhmno.
  511.      check_stopsession :-
  512.     over_priohm, !,
  513.     check_stopsession_1.
  514. %%% Otherwise, stop.
  515.      check_stopsession :-
  516.     assert_tryresult('misc_overflow').
  517.  
  518.      check_stopsession_1 :-
  519.     fixed_priority,
  520.     !,
  521.     round_spent_time,
  522.     retract(priority_bound(P)),
  523.     priority_bound_increment(I),
  524.     P1 is P+I,
  525.     assert(priority_bound(P1)),
  526.     !,
  527.     new_session.
  528.      check_stopsession_1 :-
  529.     slidepriority,
  530.     !,
  531.     check_maxhmno.
  532.  
  533. %%% Check if the number of clauses in the database exceeds a specified 
  534. %%%    number.
  535.      check_maxhmno :-
  536.     total_numhm(NumHm),
  537.     wu_bound(WU),
  538.     priority_bound(P),
  539.     max_no_clauses(MaxHMNo), !,
  540.     check_maxhmno_1(NumHm,MaxHMNo,WU).
  541.  
  542. %%% If the number of clauses in the database does not exceed a specified
  543. %%%     number.
  544.      check_maxhmno_1(NumHm,MaxHMNo,WU) :-
  545.     NumHm =< MaxHMNo, !,
  546.     round_spent_time,
  547.     Temp is 2.0 * WU,
  548.     floor(Temp,Y),
  549.     not(not(abolish(wu_bound,1))),
  550.     assert(wu_bound(Y)),
  551.     !, new_session.
  552.  
  553. %%% If the number of clauses in the database exceeds a specified
  554. %%%     number, stop.
  555.      check_maxhmno_1(_,_,_) :-
  556.     assert_tryresult('clause_no_overflow').
  557.  
  558. %%% Start a new session.
  559.      new_session :-
  560.     not(not(session_deletions)),
  561.     not(not(setup_inputs)),
  562.     session_asserts,
  563.     !, fail.
  564.  
  565. %%% Assert some initial values for a new session.
  566.      session_asserts :-
  567.     cputime(Time),
  568.     assert(round_time(Time,-1)),
  569.     assert(round_no(-1)),
  570.     inc_session,
  571.     wu_bound(S),
  572.     abolish(priority_bound,1),
  573.     assert(priority_bound(S)), 
  574.     assert(total_wu(0)),
  575.     assert(total_numhm(0)).
  576.  
  577. %%% Increase session number.
  578.      inc_session :-
  579.     retract(session_no(X)),
  580.     Y is X + 1,
  581.     assert(session_no(Y)).
  582.  
  583. %%% Use the input clauses stored at the beginning.
  584.      setup_inputs :-
  585.     slidepriority,
  586.     retract(sent_C(cl(_,_,_,0,_,_,_,_,_))),
  587.     fail.
  588.      setup_inputs :-
  589.     not(save_rewrite_rules),
  590.     !,
  591.     abolish(rwr,4),
  592.     (outrwr -> (
  593.       abolish(outrwr,0),
  594.       setup_inputs_1,
  595.       assert(outrwr)
  596.         ); setup_inputs_1).
  597.      setup_inputs.
  598.  
  599.      setup_inputs_1 :-
  600.     sent_C(cl(_,_,by([S=T],V,V,_,_),_,_,_,_,_,_)),
  601.     generate_rewrite_rule([S=T],_),
  602.     fail.
  603.      setup_inputs_1.
  604.  
  605. %%% Succeeds if a clause is not generated before.
  606.      diff_sentC1 :-
  607.     const_list(V),
  608.     sent_C(cl(_,_,by(Cn1,V11,V11,V,_),_,_,_,_,_,_)),
  609.     not(oldsentC1(Cn1)),
  610.     !.
  611.      diff_sentC1 :- fail.
  612.  
  613. %%% Update old clauses.
  614.      update_oldsentC :-
  615.     const_list(V),
  616.     current_support(Supp),
  617.     sent_C(cl(_,_,by(Cn1,V11,V11,V,_),_,Sp,_,_,_,_)),
  618.     assert_once(oldsentC(Supp,Cn1,Sp)),
  619.     fail.
  620.      update_oldsentC.
  621.  
  622. %%% Update old clauses.
  623.      update_oldsentC1 :-
  624.     not(no_repeated_clause_generation),
  625.     const_list(V),
  626.     sent_C(cl(_,_,by(Cn1,V11,V11,V,_),_,_,_,_,_,_)),
  627.     assert_once(oldsentC1(Cn1)),
  628.     fail.
  629.      update_oldsentC1.
  630.  
  631. %%% Assert support strategy for next round.
  632.      assert_new_support :-
  633.     round_no(0), !.
  634.      assert_new_support :-
  635.     get_new_supp(Supp_int,Supp),
  636.     abolish(current_support,1),
  637.     assert(current_support(Supp_int)),
  638.     write_line(5,'Support strategy: ',Supp),
  639.     !.
  640.  
  641. %%% Determine support strategy for next round.  Fail if hyper_linking is
  642. %%% complete.
  643.      get_new_supp(Supp_int,Supp) :-
  644.     saved_supp(Supp_int,Supp),
  645.     !.
  646.      get_new_supp(Supp_int,Supp) :-
  647.     retract(num_supp(N1)),
  648.     !,
  649.     N2 is N1 + 1,
  650.     get_new_supp_1(N2,N3),
  651.     get_new_supp_2(N1,N3,Supp_int,Supp,N4),
  652.     assert(num_supp(N4)),
  653.     assert(saved_supp(Supp_int,Supp)),
  654.         !.
  655.      get_new_supp(Supp_int,Supp) :-
  656.     support_list(S),
  657.     length(S,N1),
  658.     get_new_supp_2(N1,1,Supp_int,Supp,N2),
  659.     assert(num_supp(N2)),
  660.     assert(saved_supp(Supp_int,Supp)),
  661.     !.
  662.      get_new_supp_1(N1,1) :-
  663.     support_list(Supp),
  664.     length(Supp,N2),
  665.     N1 > N2,
  666.     !.
  667.      get_new_supp_1(N,N).
  668.      get_new_supp_2(N1,N2,Supp_int,Supp,N2) :-
  669.     support_list_internal(Supp_list_int),
  670.     get_list(Supp_list_int,N2,Supp_int),
  671.     get_new_supp_3(Supp_int),
  672.     support_list(Supp_list),
  673.     get_list(Supp_list,N2,Supp),
  674.     !.
  675.      get_new_supp_2(N,N,_,_,_) :-
  676.     !,
  677.     fail.
  678.      get_new_supp_2(N1,N2,Supp_int,Supp,N3) :-
  679.     N4 is N2 + 1,
  680.     get_new_supp_1(N4,N5),
  681.     !,
  682.     get_new_supp_2(N1,N5,Supp_int,Supp,N3).
  683.      get_new_supp_3(sup(_,_,_,1)) :-
  684.     const_list(Clist),
  685.     sent_C(cl(_,_,by(Cn1,V11,V11,Clist,_),_,_,_,_,_,_)),
  686.     not(oldsentC(Supp_int,Cn1,_)),
  687.     !.
  688.      get_new_supp_3(sup(Sa,Sb,Sc,0)) :-
  689.     const_list(Clist),
  690.     sent_C(cl(_,_,by(Cn1,V11,V11,Clist,_),_,sp(S1a,S1b,S1c),_,_,_,_)),
  691.     get_new_supp_4([Sa,Sb,Sc],[S1a,S1b,S1c],[S2a,S2b,S2c]),
  692.     not(oldsentC(Supp_int,Cn1,sp(S2a,S2b,S2c))),
  693.     !.
  694.      get_new_supp_4([],[],[]).
  695.      get_new_supp_4([0|Ss1],[_|Ss2],[_|Ss3]) :-
  696.     !,
  697.     get_new_supp_4(Ss1,Ss2,Ss3).
  698.      get_new_supp_4([1|Ss1],[S|Ss2],[S|Ss3]) :-
  699.     !,
  700.     get_new_supp_4(Ss1,Ss2,Ss3).
  701.  
  702. %%% Compute starting work unit bound.
  703. %%% If the starting work unit bound is specified by the user, done.
  704.      compute_start_wu(WU) :-
  705.     start_wu_bound(WU), WU \== 0, !.
  706. %%% Otherwise, compute it.
  707.      compute_start_wu(WU) :-
  708.     compute_start_wu_1(Size,Depth,Literal),
  709.     size_coef(C1),
  710.     depth_coef(C2),
  711.     literal_coef(C3),
  712.     relevance_coef(C4),
  713.     get_start_no_clauses(ST),
  714.     T1 is Size*C1,
  715.     floor(T1,KK1),
  716.     T2 is Depth*C2,
  717.     floor(T2,KK2),
  718.     T3 is Literal*C3,
  719.     floor(T3,KK3),
  720.     T4 is 4*C4,
  721.     floor(T4,KK4),
  722.     maximum(KK1,KK2,Temp1),
  723.     maximum(Temp1,KK3,Temp2),
  724.     maximum(Temp2,KK4,Temp3),
  725.     WU is ST * Temp3.
  726.  
  727.      compute_start_wu_1(Size,Depth,Literal) :-
  728.     bagof1(R,C^clause(sent_C(C),true,R),Rs),
  729.     compute_start_wu_1(Rs,Size,Depth,Literal).
  730.     
  731.      compute_start_wu_1([R|Rs],SO,DO,LO) :-
  732.     clause(sent_C(cl(_,_,by(Cn,_,_,_,_),_,_,_,_,_,_)),true,R),
  733.     max_clausesize_sp(Cn,S1),
  734.     clause_depth(Cn,D1),
  735.     length(Cn,L1),
  736.     compute_start_wu_2(Rs,S1,D1,L1,SO,DO,LO).
  737.  
  738.      compute_start_wu_2([R|Rs],S1,D1,L1,SO,DO,LO) :-
  739.     clause(sent_C(cl(_,_,by(Cn,_,_,_,_),_,_,_,_,_,_)),true,R), 
  740.     max_clausesize_sp(Cn,SM1),
  741.     clause_depth(Cn,DM1),
  742.     length(Cn,LM),
  743.     maximum(S1,SM1,SN2),
  744.     maximum(D1,DM1,DN2),
  745.     maximum(L1,LM,LN2),
  746.     !,
  747.     compute_start_wu_2(Rs,SN2,DN2,LN2,SO,DO,LO).
  748.      compute_start_wu_2([],SO,DO,LO,SO,DO,LO).
  749.  
  750.      get_start_no_clauses(ST) :-
  751.     start_no_clauses(ST), !.
  752.      get_start_no_clauses(ST) :-
  753.     start_no_clauses_ceof(X),
  754.     !, 
  755.     number_inclauses(IN),
  756.     ST is X * IN, !.
  757.      get_start_no_clauses(ST) :-
  758.     number_inclauses(IN),
  759.     ST is 3 * IN.
  760.